Search Results

Documents authored by Doumane, Amina

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.121
Regular Expressions for Tree-Width 2 Graphs

Authors: Amina Doumane

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We propose a syntax of regular expressions, which describes languages of tree-width 2 graphs. We show that these languages correspond exactly to those languages of tree-width 2 graphs, definable in the counting monadic second-order logic (CMSO).
Cite as

Amina Doumane. Regular Expressions for Tree-Width 2 Graphs. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 121:1-121:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.ICALP.2022.121,
  author =	{Doumane, Amina},
  title =	{{Regular Expressions for Tree-Width 2 Graphs}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{121:1--121:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.121},
  URN =		{urn:nbn:de:0030-drops-164627},
  doi =		{10.4230/LIPIcs.ICALP.2022.121},
  annote =	{Keywords: Tree width, MSO, Regular expressions}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2021.1
Non-Axiomatizability of the Equational Theories of Positive Relation Algebras (Invited Talk)

Authors: Amina Doumane

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
In the literature, there are two ways to show that the equational theory of relations over a given signature is not finitely axiomatizable. The first-one is based on games and a construction called Rainbow construction. This method is very technical but it shows a strong result: the equational theory cannot be axiomatized by any finite set of first-order formulas. There is another method, based on a graph characterization of the equational theory of relations, which is easier to get and to understand, but proves a weaker result: the equational theory cannot be axiomatized by any finite set of equations. In this presentation, I will show how to complete the second technique to get the stronger result of non-axiomatizability by first-order formulas.
Cite as

Amina Doumane. Non-Axiomatizability of the Equational Theories of Positive Relation Algebras (Invited Talk). In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.MFCS.2021.1,
  author =	{Doumane, Amina},
  title =	{{Non-Axiomatizability of the Equational Theories of Positive Relation Algebras}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.1},
  URN =		{urn:nbn:de:0030-drops-144417},
  doi =		{10.4230/LIPIcs.MFCS.2021.1},
  annote =	{Keywords: Relation algebra, Graph homomorphism, Equational theories, First-order logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.41
Graph Characterization of the Universal Theory of Relations

Authors: Amina Doumane

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The equational theory of relations can be characterized using graphs and homomorphisms. This result, found independently by Freyd and Scedrov and by Andréka and Bredikhin, shows that the equational theory of relations is decidable. In this paper, we extend this characterization to the whole universal first-order theory of relations. Using our characterization, we show that the positive universal fragment is also decidable.
Cite as

Amina Doumane. Graph Characterization of the Universal Theory of Relations. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.MFCS.2021.41,
  author =	{Doumane, Amina},
  title =	{{Graph Characterization of the Universal Theory of Relations}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{41:1--41:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.41},
  URN =		{urn:nbn:de:0030-drops-144815},
  doi =		{10.4230/LIPIcs.MFCS.2021.41},
  annote =	{Keywords: Relation algebra, Graph homomorphism, Equational theories, First-order logic}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.29
Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms

Authors: Amina Doumane and Damien Pous

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study the equational theories of composition and intersection on binary relations, with or without their associated neutral elements (identity and full relation). Without these constants, the equational theory coincides with that of semilattice-ordered semigroups. We show that the equational theory is no longer finitely based when adding one or the other constant, refuting a conjecture from the literature. Our proofs exploit a characterisation in terms of graphs and homomorphisms, which we show how to adapt in order to capture standard equational theories over the considered signatures.
Cite as

Amina Doumane and Damien Pous. Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{doumane_et_al:LIPIcs.CONCUR.2020.29,
  author =	{Doumane, Amina and Pous, Damien},
  title =	{{Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.29},
  URN =		{urn:nbn:de:0030-drops-128411},
  doi =		{10.4230/LIPIcs.CONCUR.2020.29},
  annote =	{Keywords: Relation algebra, graph homomorphisms, (in)equational theories}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.18
Completeness for Identity-free Kleene Lattices

Authors: Amina Doumane and Damien Pous

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.
Cite as

Amina Doumane and Damien Pous. Completeness for Identity-free Kleene Lattices. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doumane_et_al:LIPIcs.CONCUR.2018.18,
  author =	{Doumane, Amina and Pous, Damien},
  title =	{{Completeness for Identity-free Kleene Lattices}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.18},
  URN =		{urn:nbn:de:0030-drops-95564},
  doi =		{10.4230/LIPIcs.CONCUR.2018.18},
  annote =	{Keywords: Kleene algebra, Graph languages, Petri Automata, Kleene theorem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.42
Infinitary Proof Theory: the Multiplicative Additive Case

Authors: David Baelde, Amina Doumane, and Alexis Saurin

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.
Cite as

David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CSL.2016.42,
  author =	{Baelde, David and Doumane, Amina and Saurin, Alexis},
  title =	{{Infinitary Proof Theory: the Multiplicative Additive Case}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42},
  URN =		{urn:nbn:de:0030-drops-65825},
  doi =		{10.4230/LIPIcs.CSL.2016.42},
  annote =	{Keywords: Infinitary proofs, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.549
Least and Greatest Fixed Points in Ludics

Authors: David Baelde, Amina Doumane, and Alexis Saurin

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators. In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data. We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).
Cite as

David Baelde, Amina Doumane, and Alexis Saurin. Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 549-566, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CSL.2015.549,
  author =	{Baelde, David and Doumane, Amina and Saurin, Alexis},
  title =	{{Least and Greatest Fixed Points in Ludics}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{549--566},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.549},
  URN =		{urn:nbn:de:0030-drops-54374},
  doi =		{10.4230/LIPIcs.CSL.2015.549},
  annote =	{Keywords: proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact